es:ES, k:Knd, l:IdLnk, tg:Id, ds:x:Id fp Type, da:k:Knd fp Type, n:, a:ecl(ds;da),
f:(State(ds)Valtype(da;k)da(rcv(l,tg))?Void).
es-decls(es;source(l);ds;da)
 (with decls ds 
 (with decls da
 (sends on l from e 
 (include if kind(e) = k  action[[a n]][es-init(es;e);e] [<tg,f((state when e),val(e))>]
 (include else nil fi 
 (and only these for tags in [tg]
 (
 (es-sends-iff2(es;l;tg;da(rcv(l,tg))?Top;ds;e.kind(e) = k
 (& ecl-es-act(es;n;a)(es-init(es;e),e);e.f((state when e),val(e)))) 

latex

Definitions

x. t(x), P  Q, t  T, P & Q, P  Q, P  Q, x:A. B(x), A & B, es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e)), Prop, {T}, SQType(T), P  Q, e@i. P(e), Valtype(da;k), x:A. B(x), True, T, with decls ds dasends on l from e include f(e) and only these for tags in tgs, false, true, if b t else f fi, f(x)?z, state@i, x(s1,s2), State(ds), False, Y, p  q, ||as||, e  e' , i<j, b, ij, nth_tl(n;as), hd(l), l[i], x(s), {i..j}, Unit, , A, AB, i  j < k, ,

Lemmas

event system wf, IdLnk wf, Id wf, fpf wf, nat wf, ecl wf, rcv wf, Kind-deq wf, Knd wf, fpf-cap wf, ma-valtype wf, decl-state wf, lsrc wf, es-decls wf, es-decls-iff, es-kind wf, es-loc wf, es-kind-rcv, Knd sq, es-loc-init, es-init wf, es-valtype wf, es-isrcv wf, assert wf, ecl-es-act wf, es-lnk wf, es-sender wf, es-tag wf, member singleton, l member wf, assert of bnot, or functionality wrt iff, assert of bor, bnot thru band, eqff to assert, not wf, bnot wf, bor wf, non neg length, es-sends wf, es-Msgl wf, length wf1, int seg wf, es-index wf, assert of band, eqtt to assert, iff transitivity, bool wf, bool sq, es-loc-rcv, es-E wf, ldst wf, true wf, squash wf, es-bact wf, eq knd wf, band wf, bool cases, same-sender-index, es-rcv-kind, fpf-ap wf, fpf-trivial-subtype-top, fpf-dom wf, subtype rel transitivity, subtype rel self, id-deq wf, es-vartype wf, subtype rel dep function, es-state-when wf, es-loc-sender, assert-eq-knd, assert-es-bact, es-locl wf, es-index-zero, Id sq